package src;

import java.util.ArrayList;
import java.util.HashMap;

public class FOL {
	final static String FORALL = "%";
	final static String THERE_EXISTS = "$";
	final static String AND = "&";
	final static String OR = "|";
	final static String NOT = "!";
	final static String IF_ONLY_IF = "=";
	final static String IMPLIES = ">";
	final static String LEFT_SQUARE_BRACKET = "[";
	final static String RIGHT_SQUARE_BRACKET = "]";
	final static String LEFT_BRACE = "(";
	final static String RIGHT_BRACE = ")";
	final static String RIGHT_CURLY_BRACE = "}";
	final static String LEFT_CURLY_BRACE = "{";
	static int numVar = 0;

	/**
	 * Given an array of strings, start index and end index it returns a string
	 * representation of the elements in the array separated by a space
	 * 
	 * @param startIndex
	 * @param endIndex
	 * @param input
	 * @return String
	 */
	public static String getString(int startIndex, int endIndex, String[] input) {
		String result = "";
		for (int i = startIndex; i <= endIndex; i++) {
			if (input[i].equals(""))
				continue;
			if (i == startIndex)
				result = input[i];
			else
				result = result + " " + input[i];
		}
		return result;
	}

	/**
	 * Given a string as input this method returns a string with the implication
	 * replaced by its equivalent form of ! and or
	 * 
	 * @param input
	 * @return String
	 */
	public static String removeImplication(String input) {
		String result = "";
		String[] firstSplitArr = input.split(" ");
		for (int i = 0; i < firstSplitArr.length; i++) {
			String current = firstSplitArr[i];
			if (current.equals(IMPLIES)) {
				int firstClauseIndex = getClause(firstSplitArr, i, true); // Index
																			// of
																			// the
																			// first
																			// term
																			// in
																			// the
																			// first
																			// clause
				int secClauseIndex = getClause(firstSplitArr, i, false); // Index
																			// of
																			// last
																			// term
																			// in
																			// the
																			// second
																			// clause
				String s1 = getString(firstClauseIndex, i - 1, firstSplitArr);// Precedent
																				// of
																				// implication
				String s2 = getString(i + 1, secClauseIndex, firstSplitArr);// antecedent
																			// of
																			// implication
				result = getString(0, firstClauseIndex - 1, firstSplitArr)
						+ " "
						+ NOT
						+ " "
						+ s1
						+ " "
						+ OR
						+ " "
						+ s2
						+ " "
						+ getString(secClauseIndex + 1,
								firstSplitArr.length - 1, firstSplitArr);
				return result;
			}
		}
		return result;
	}

	/**
	 * Given a string as input this method returns a logically equivalent string
	 * with if only if removed and replaced by the double implication notation
	 * 
	 * @param input
	 * @return String
	 */
	public static String removeIfAndOnlyIf(String input) {
		String result = "";
		String[] firstSplitArr = input.split(" ");
		for (int i = 0; i < firstSplitArr.length; i++) {
			String current = firstSplitArr[i];
			if (current.equals(IF_ONLY_IF)) {
				int firstClauseIndex = getClause(firstSplitArr, i, true); // Index
																			// of
																			// the
																			// first
																			// term
																			// in
																			// the
																			// first
																			// clause
				int secClauseIndex = getClause(firstSplitArr, i, false); // Index
																			// of
																			// last
																			// term
																			// in
																			// the
																			// second
																			// clause
				String s1 = getString(firstClauseIndex, i - 1, firstSplitArr);
				String s2 = getString(i + 1, secClauseIndex, firstSplitArr);
				result = getString(0, firstClauseIndex - 1, firstSplitArr)
						+ " ( "
						+ s1
						+ " "
						+ IMPLIES
						+ " "
						+ s2
						+ " ) "
						+ AND
						+ " ( "
						+ s2
						+ " "
						+ IMPLIES
						+ " "
						+ s1
						+ " ) "
						+ getString(secClauseIndex + 1,
								firstSplitArr.length - 1, firstSplitArr);
				return result;
			}
		}
		return result;
	}

	public static String getCNF(String input) {
		while (input.contains(IF_ONLY_IF)) {
			input = removeIfAndOnlyIf(input);
		}
		while (input.contains(IMPLIES)) {
			input = removeImplication(input);
		}
		input = pushNotInwards(input);
		input = renameVariables(input);
		
		if(input.contains(THERE_EXISTS))
		input = skelomize(input);
		
		input = discardUQ(input);
		input = flatten(input);
		input = CNFI(input);
		
		return input;
	}

	/**
	 * If isFirst is true this method returns the index of the first element in
	 * the clause before the index. If isFirst is true thie method returns the
	 * index of the last element in the clause after the index.
	 * 
	 * @param input
	 * @param index
	 *            is the index element before or after a clause (could be the
	 *            index of an operator)
	 * @param isFirst
	 *            a boolean to indicate if we want the precedent or antecedent
	 *            of the operator clause
	 * @return int
	 */
	public static int getClause(String[] input, int index, boolean isFirst) {

		if (isFirst) {
			if (input[index - 1].equals(RIGHT_BRACE)) {
				return getClauseHelper(input, RIGHT_BRACE, LEFT_BRACE, true,
						index - 1);
			}
			if (input[index - 1].equals(RIGHT_SQUARE_BRACKET)) {
				return getClauseHelper(input, RIGHT_SQUARE_BRACKET,
						LEFT_SQUARE_BRACKET, true, index - 1);
			}
			if (input[index - 1].equals(RIGHT_CURLY_BRACE)) {
				return getClauseHelper(input, RIGHT_CURLY_BRACE,
						LEFT_CURLY_BRACE, true, index - 1);
			}
			return index - 1;

		} else {
			if (input[index + 1].equals(LEFT_BRACE)) {
				return getClauseHelper(input, RIGHT_BRACE, LEFT_BRACE, false,
						index + 1);
			}
			if (input[index + 1].equals(LEFT_SQUARE_BRACKET)) {
				return getClauseHelper(input, RIGHT_SQUARE_BRACKET,
						LEFT_SQUARE_BRACKET, false, index + 1);
			}
			if (input[index + 1].equals(LEFT_CURLY_BRACE)) {
				return getClauseHelper(input, RIGHT_CURLY_BRACE,
						LEFT_CURLY_BRACE, false, index + 1);
			}
			return index + 1;

		}
	}

	// Insetead of having code twice send start and endm, check if start>end to
	// know if ++ or --
	// Given a certain brace gets the clause, direction indicates to go left or
	// right
	// index is the index of the brace
	/**
	 * 
	 * 
	 * @param input
	 * @param rightBrace
	 * @param leftBrace
	 * @param goLeft
	 *            A boolean variable tp define the direction of searching
	 *            (whether am getting the right clause or the left clause)
	 * @param index
	 *            The index of the brace
	 * @return
	 */
	public static int getClauseHelper(String[] input, String rightBrace,
			String leftBrace, boolean goLeft, int index) {
		int numLeft = 0;
		int numRight = 0;
		if (goLeft) {
			numRight++;
			String current = "";
			for (int i = index - 1; i >= 0; i--) {
				current = input[i];

				if (current.equals(rightBrace)) {
					numRight++;
				} else {
					if (current.equals(leftBrace)) {
						numLeft++;
					}
				}
				if (numLeft == numRight) {
					return i;

				}

			}
		} else {
			numLeft++;
			String current = "";
			for (int i = index + 1; i < input.length; i++) {
				current = input[i];
				if (current.equals(rightBrace)) {
					numRight++;
				} else {
					if (current.equals(leftBrace)) {
						numLeft++;
					}
				}
				if (numLeft == numRight) {
					return i;

				}

			}

		}
		return -1;
	}

	public static String applyDeMorganNot(String input) {
		String[] splitArr = input.split(" ");
		if (splitArr.length == 1)
			return splitArr[0];
		if (splitArr.length == 2 && splitArr[0].equals(NOT))
			return splitArr[0] + " " + splitArr[1];
		HashMap<Integer, Integer> clauseIndices = new HashMap<Integer, Integer>();
		for (int i = 0; i < splitArr.length; i++) {
			if (splitArr[i].equals(NOT)) {
				int notClauseIndex = getClause(splitArr, i, false);
				for (int j = i + 1; j < notClauseIndex - 1; j++) { // This is to
																	// loop on
																	// all
																	// possible
																	// clauses
																	// inside
																	// the not
																	// clause
					int index = getClause(splitArr, j, false);
					clauseIndices.put(new Integer(j + 1), new Integer(index));// This
																				// is
																				// a
																				// hashmap
																				// to
																				// hold
																				// the
																				// start
																				// and
																				// end
																				// of
																				// all
																				// clauses
																				// inside
																				// the
																				// not
																				// clause
					j = index;
					// j--;
					if (splitArr[index + 1].equals(AND)) {
						splitArr[index + 1] = OR;

					} else {
						if (splitArr[index + 1].equals(OR)) {
							splitArr[index + 1] = AND;

						}

					}

				}
				ArrayList<Integer> keys = new ArrayList<Integer>(
						clauseIndices.keySet());
				String result = "";
				if (keys.size() != 0)
					result = result + getString(0, i - 1, splitArr) + " "
							+ getString(i + 1, keys.get(0) - 1, splitArr) + " "
							+ ApplyDeMorganOnAll(clauseIndices, splitArr);

				else
					result = result + getString(0, i, splitArr);
				if (notClauseIndex != splitArr.length - 1)
					result = result
							+ " "
							+ applyDeMorganNot(getString(notClauseIndex,
									splitArr.length - 1, splitArr));
				return result;
			}
		}
		return getString(0, splitArr.length - 1, splitArr);
	}

	public static String ApplyDeMorganOnAll(
			HashMap<Integer, Integer> clauseIndices, String[] splitArr) {
		String result = "";
		ArrayList<Integer> keys = new ArrayList<Integer>(clauseIndices.keySet());
		for (int i = 0; i < keys.size(); i++) {
			Integer startIndex = keys.get(i);
			Integer endIndex = clauseIndices.get(startIndex);
			result = result
					+ " "
					+ applyDeMorganNot(NOT + " "
							+ getString(startIndex, endIndex, splitArr));
			if (endIndex != splitArr.length - 1) {
				result = result + " " + splitArr[endIndex + 1];
			}

		}
		return result;
	}

	public static ArrayList<String> mySplitFunc(String input) {
		ArrayList<String> result = new ArrayList<String>();
		String prev = input.charAt(0) + "";
		for (int i = 1; i < input.length(); i++) {
			System.out.println("prev is" + prev + "*");
			if (input.charAt(i) == ' ') {
				result.add(prev);
				prev = "";
			} else {
				prev = prev + input.charAt(i);
			}
		}
		return result;
	}

	public static String removeDoubleNot(String input) {

		String[] splitArr = input.split(" ");
		String[] result = removeDoubleNotHelper(splitArr, 0);
		return getString(0, result.length - 1, result);
	}

	public static String[] removeDoubleNotHelper(String[] input, int index) {
		if (index == input.length)
			return input;
		if ((input[index]).equals(NOT)) {
			if ((index != input.length - 1) && (input[index + 1]).equals(NOT)) {
				input[index] = "";
				input[index + 1] = "";
			}
		}
		return removeDoubleNotHelper(input, index + 1);

	}

	public static String pushNotInwards(String input) {
		String prev = "";
		String current = input;
		while (!prev.equals(current)) {

			prev = current;
			current = notQuantifierHandler(applyDeMorganNot(removeDoubleNot(current)));

		}
		return current;
	}

	/**
	 * Method responsible for renaming variables
	 * 
	 * @param input
	 * @return
	 */
	public static String renameVariables(String input) {
		String[] splitArr = input.split(" ");
		HashMap<String, String> mappings = new HashMap<String, String>();// Hashmap
																			// with
																			// the
																			// variables
																			// and
																			// the
																			// chars
																			// with
																			// which
																			// they
																			// were
																			// replace
																			// this
																			// is
																			// to
																			// keep
																			// track
																			// of
																			// which
																			// variables
																			// are
																			// used
		for (int i = 0; i < splitArr.length; i++) {
			if (splitArr[i].equals(FORALL) || splitArr[i].equals(THERE_EXISTS)) {
				String variables = splitArr[i + 1];// Variables quantified by
													// the quantifier
				int clauseIndex = getClause(splitArr, i + 1, false);// The index
																	// of the
																	// last
																	// element
																	// in the
																	// scop of
																	// the
																	// quantifier
																	// (The
																	// bracket
																	// that
																	// closes
																	// the
																	// quanitifier's
																	// scope)
				for (int j = 0; j < variables.length(); j++) {
					String currChar = variables.charAt(j) + "";
					String temp = variables.charAt(j) + "";
					char replacement = 123; // unicode for char after z
											// Start form z and move up the
											// alphabet until a suitable unused
											// replacement is found
					while (mappings.containsKey(currChar)) {

						replacement--;
						currChar = replacement + "";
					}
					mappings.put(temp, currChar);
					for (int k = i; k <= clauseIndex; k++) {

						splitArr[k] = splitArr[k].replaceAll(temp, currChar);
					}
				}
			}
		}
		return getString(0, splitArr.length - 1, splitArr);
	}

	 
	 /**
	 * The method takes a FOL expression and removes all existential quantifiers and replace
	 * their variables with skelom functions of the variables of the universal quantifiers
	 * that the existential quantifier is in their scope
	 * @param input string representing a FOL expression
	 * @return expression after skelomization step
	 */
	
	public static String skelomize(String input) {
		
		
		int skelomFunCounter = 0;
		String[] splitArr = input.split(" ");
		boolean foundForAll = false;
		for (int i = 0; i < splitArr.length; i++) {
			String current = splitArr[i];
			if(current.equals(FORALL))
				foundForAll = true;
			if (current.equals(THERE_EXISTS)) {
				splitArr[i] = "";
				String variables = splitArr[i + 1];
				splitArr[i + 1] = "";
				int variablesNum = variables.length();
				int endScope = getClause(splitArr, i + 1, false);
				String UQvariables = getUQVariable(splitArr, endScope);
				String skelomFun = "(";
				for (int t = 0; t < UQvariables.length(); t++) {
					if (t == UQvariables.length() - 1)
						skelomFun += UQvariables.charAt(t) + "";
					else
						skelomFun += UQvariables.charAt(t) + ",";
				}

				for (int v = 0; v < variablesNum; v++) {
					skelomFunCounter++;
					String currentVar = variables.charAt(v) + "";
					String skelomFun2 = "F" + skelomFunCounter + skelomFun
							+ ")";
					if(!foundForAll)
						skelomFun2 = "F" + skelomFunCounter;
					for (int j = i + 3; j < endScope; j++) {
						splitArr[j] = splitArr[j].replaceAll(currentVar,
								skelomFun2);
					}
				}

			}
		}

		return getString(0, splitArr.length - 1, splitArr);
	}

	/**
	 * Helper method used by skelomize method, it takes a FOL expression and the index
	 * of an existential quantifier and returns all the variables 
	 * that are universally quantified and the existential quantifier is in their scope.
	 * @param input array of string representing FOL expression
	 * @param index of an existential quantifier
	 * @return string of representing the concatenation of variables
	 */
	 
	
	public static String getUQVariable(String[] input, int index) {
		String res = "";
		for (int i = 0; i < index; i++) {
			String current = input[i];
			if (current.equals(FORALL)) {

				int scope = getClause(input, i + 1, false);
				if (scope > index)
					res += input[i + 1];
			}

		}
		return res;
	}

	/**
	 * The method takes a FOL expression and drops all the universal quantifiers in the sentence
	 * @param input string representing FOL expression
	 * @return expression after dropping universal quantifiers
	 */
	
	public static String discardUQ(String input) {
		String[] splitArr = input.split(" ");
		for (int i = 0; i < splitArr.length - 1; i++) {
			String current = splitArr[i];
			if (current.equals(FORALL)) {
				splitArr[i] = "";
				splitArr[i + 1] = "";			
			}
		}
		return getString(0, splitArr.length - 1, splitArr);
	}
	/**
	 * the method takes a string and replaces all square brackets with normal braces
	 * and removes the space between the not (!) and the literals (to simplify string processing
	 * in following steps)
	 * @param input string representing the FOL expression
	 * @return string of the modified expression
	 */
	public static String normalize(String input) {
		String[] splitArr = input.split(" ");
		for (int i = 0; i < splitArr.length; i++) {
			String current = splitArr[i];
			if (current.equals(NOT)) {
				splitArr[i] = "";
				splitArr[i + 1] = "!" + splitArr[i + 1];
			} else if (current.equals(LEFT_SQUARE_BRACKET))
				splitArr[i] = LEFT_BRACE;
			else if (current.equals(RIGHT_SQUARE_BRACKET))
				splitArr[i] = RIGHT_BRACE;
		}
		// String result = getString(0, splitArr.length-1, splitArr);
		// return removeExtraSpaces(result);
		return getString(0, splitArr.length - 1, splitArr);
	}

	/**
	 * The method takes a FOL expression and for every occurrence of double brackets around 
	 * subexpression in the expression, it removes one of them. 
	 * @param input string representing the FOL expression
	 * @return string of the expression after removing double brackets
	 */
	
	
	public static String removeDoubleBrackets(String input) {
		String[] splitArr = input.split(" ");
		for (int i = 0; i < splitArr.length; i++) {
			if (splitArr[i].equals(LEFT_BRACE)
					&& splitArr[i + 1].equals(LEFT_BRACE)) {
				int endIndex1 = getClause(splitArr, i - 1, false);
				int endIndex2 = getClause(splitArr, i, false);
				// System.out.println(i+","+ (endIndex1) );
				// System.out.println((i+1)+","+ (endIndex2) );
				if (endIndex1 == endIndex2 + 1) {
					splitArr[i] = "";
					splitArr[endIndex1] = "";
				}
			}
		}
		String result = getString(0, splitArr.length - 1, splitArr);
		return removeExtraSpaces(result);
	}

	/**
	 * The method takes a FOL expression and flattens subexpression of conjuncted literals 
	 * @param startIndex of the subexpression to flatten
	 * @param endIndex of the subexpression to flatten
	 * @param input array of strings representing FOL sentence
	 * @return array of strings representing sentence after modification
	 */
	
	public static String[] flattenAnd(int startIndex, int endIndex,
			String[] input) {
		for (int i = startIndex; i <= endIndex; i++) {
			if (input[i].equals(OR))
				return input;
		}

		for (int i = startIndex+1 ; i < endIndex; i++) {
			if (input[i].equals(LEFT_BRACE) || input[i].equals(RIGHT_BRACE))
				input[i] = "";
		}
		return input;

	}

	/**
	 * The method takes a FOL expression and flattens subexpression of disjuncted literals 
	 * @param startIndex of the subexpression to flatten
	 * @param endIndex of the subexpression to flatten
	 * @param input array of strings representing FOL sentence
	 * @return array of strings representing sentence after modification
	 */
	
	public static String[] flattenOR(int startIndex, int endIndex,
			String[] input) {
		for (int i = startIndex; i <= endIndex; i++) {
			if (input[i].equals(AND))
				return input;
		}

		for (int i = startIndex+1 ; i < endIndex; i++) {
			if (input[i].equals(LEFT_BRACE) || input[i].equals(RIGHT_BRACE))
				input[i] = "";
		}
		// String temp = getString(startIndex, endIndex, input);
		// System.out.println(temp);
		return input;

	}

	 /**
	 * The method takes a FOL sentence and flattens all subexpressions
	 * of only conjunctions and only disjunctions in the sentence.
	 * @param input string representing FOL sentence
	 * @return modified sentence
	 */
	
	public static String flattenAndOr(String input) {
		String[] splitArr = input.split(" ");
		for (int i = 0; i < splitArr.length; i++) {
			String current = splitArr[i];
			// System.out.println("cell: "+i+" , "+ current);
			if (current.equals(LEFT_BRACE)) {
				int endIndex = getClause(splitArr, i - 1, false);
				// System.out.println(i+" "+current+" endIndex: "+endIndex+"....."+splitArr[endIndex]);
				splitArr = flattenAnd(i, endIndex, splitArr);
				splitArr = flattenOR(i, endIndex, splitArr);
			}
		}
		String result = getString(0, splitArr.length - 1, splitArr);
		return removeExtraSpaces(result);
	}

	/**
	 * Helper method used to remove extra spaces in the FOL expression
	 * @param input string representing FOL expression
	 * @return string of the expression after the modification
	 */
	
	public static String removeExtraSpaces(String input) {
		String[] splitArr = input.split(" ");
		int counter = 0;
		for (int i = 0; i < splitArr.length; i++) {
			if (splitArr[i].equals(""))
				counter++;
		}

		String[] newArr = new String[splitArr.length - counter];
		counter = 0;
		for (int i = 0; i < splitArr.length; i++) {
			if (splitArr[i].equals("") == false) {
				newArr[counter++] = splitArr[i];
				// System.out.println(splitArr[i]);
			}
		}
		return getString(0, newArr.length - 1, newArr);
	}

	/**
	 * The method takes a FOL expression and applies demorgan's law and Flatten nested 
	 * conjunctions and disjunctions using the commutativity and associativity of or and and.
	 * @param input string representing FOL expression
	 * @return expression consisting of conjunction of disjunctions
	 */
	
	public static String flatten(String input) {
		System.out.println("--------------");
		System.out.println(input);
		input = removeExtraSpaces(input);
		input = normalize(input);
		System.out.println(input + "..after normalizing");
		String input2 = removeDoubleBrackets(input);
		System.out.println(input2 + "...after removing the extra brackets");
		input2 = flattenAndOr(input2);
		System.out.println(input2 + "...after flattening ");

		String[] splitArr = input2.split(" ");

		String input3 = input2;
		for (int i = 0; i < splitArr.length; i++) {

			if (splitArr[i].equals(OR) && splitArr[i + 1].equals(LEFT_BRACE)) {
				int endIndex = getClause(splitArr, i, false);
				int beforeOr = getClause(splitArr, i, true);
				String x = "";
				for(int m = beforeOr; m<i-1; m++)
					x+=splitArr[m] + " ";
				x+=splitArr[i-1];
				
				String s = applyDemorganOR(x, i + 1, endIndex, splitArr);
				
				input3= "";
					   
				   
				   for(int j = 0; j<beforeOr ; j++)
					   input3+=splitArr[j]+" ";
				   input3+=s;
				   for(int j = endIndex+1; j<splitArr.length ; j++)
					   input3+=splitArr[j]+" ";
				   
				   input3 = flattenAndOr(removeDoubleBrackets(removeExtraSpaces(input3)));
			       
				   if(input3.contains("| ("))
					   return flatten(input3);
				   else
					   break;


			}
		}

		// System.out.println(input);
		return input3;

	}

	/**
	 * The method applies Demorgan's rule of distributing or over and
	 * A or ( B and C ... ) = (A or B) and (A or C)...
	 * @param x index of literal before or (A)
	 * @param startIndex of the clause after the or
	 * @param endIndex of the clause after the or
	 * @param input string representing FOL expression
	 * @return string of subexpression after distributing or over and
	 */
	
	public static String applyDemorganOR(String x, int startIndex, int endIndex,
			String[] input) {
		// ArrayList args = new ArrayList();
		String res = "";
		String temp = getString(startIndex + 1, endIndex - 1, input);
		String[] args = temp.split("&");

		for (int i = 0; i < args.length; i++) {
			System.out.println(args[i] + ", ana args of i");
			if (i == args.length - 1)
				res += "( " + args[i] + " | " + x + " ) ";
			else
				res += "( " + args[i] + " | " + x + " ) & ";
		}
		// System.out.println(res);
		return res;
	}

	/**
	 * This method takes a part of the FOL expression and determines if it's a flat sentence
	 * or not. it returns false if the expression within the indices contains nested expression
	 * @param input array of strings in the FOL expression
	 * @param startIndex of the sub expression
	 * @param endIndex of the sub expression
	 * @return false if not flat, true if flat.
	 */
		
	public static boolean flat(String[] input, int startIndex, int endIndex) {
		for (int i = startIndex + 1; i < endIndex; i++) {
			String current = input[i];
			if (input[i].equals(LEFT_BRACE) || input[i].equals(RIGHT_BRACE)) {
				return false;
			}
		}
		return true;
	}

	/**
	 * This method performs steps 8 ( transforming into CNF set of clauses) works by replacing
	 * each "&" and "|" by "," and braces by curly braces, And adding the result between two curly
	 * braces so that the sentence is a set of clauses. 
	 * @param input sentence in the form of conjunction of disjunctions
	 * @return sentence in clause form.
	 */
	
	public static String CNFI(String input) {
		String[] splitArr = input.split(" ");
		for (int i = 0; i < splitArr.length; i++) {
			if (splitArr[i].equals(LEFT_BRACE))
				splitArr[i] = "{";
			if (splitArr[i].equals(RIGHT_BRACE))
				splitArr[i] = "}";
			if (splitArr[i].equals(AND))
				splitArr[i] = ",";
			if (splitArr[i].equals(OR))
				splitArr[i] = ",";
		}

		String result = getString(0, splitArr.length - 1, splitArr);
	//	result = "{ " + result + " }";
		return result;
	}

	public static String notQuantifierHandler(String input) {
		String[] splitArr = input.split(" ");
		for (int i = 0; i < splitArr.length; i++) {
			if (splitArr[i].equals(NOT)) {
				if (splitArr[i + 1].equals(FORALL)) {
					splitArr[i] = THERE_EXISTS;
					splitArr[i + 1] = splitArr[i + 2];
					return (getString(0, i - 1, splitArr) + " " + splitArr[i]
							+ " " + splitArr[i + 1] + " " + NOT + " " + notQuantifierHandler(getString(
								i + 3, splitArr.length - 1, splitArr))).trim();
				} else {
					if (splitArr[i + 1].equals(THERE_EXISTS)) {
						splitArr[i] = FORALL;
						splitArr[i + 1] = splitArr[i + 2];
						return (getString(0, i - 1, splitArr) + " "
								+ splitArr[i] + " " + splitArr[i + 1] + " "
								+ NOT + " " + notQuantifierHandler(getString(
									i + 3, splitArr.length - 1, splitArr)))
								.trim();
					}
				}
			}
		}
		return getString(0, splitArr.length - 1, splitArr);
	}

	// input { { P(x) , q(x) } , { l(x) , t(x) } }
	public static String standardizeApart(String input) {

		String[] splitArr = input.split(" ");
		HashMap<String, String> varMap = new HashMap<String, String>();
		String result = "";
		for (int i = 0; i < splitArr.length -1; i++) {

			int clauseIndex = getClause(splitArr, i, false);
			result = result+splitArr[i]+" ";
			String clause = getString(i + 1, clauseIndex, splitArr);
			varMap = getVariables(clause);
			for (int j = 0; j < clause.length(); j++) {
				String current = clause.charAt(j) + "";
				System.out.println("current s s "+current);
				if (varMap.containsKey(current)) {
					result = result + varMap.get(current);
				} else
					result = result + current;
				//System.out.println("splitArr[j] " + splitArr[j]);

			}
			result = result +" ";
			i = clauseIndex;
			
		}
		//return getString(0, splitArr.length - 1, splitArr);
		return result+splitArr[splitArr.length-1];

	}

	// input = { Q( f(x) , z ) , p(y) }
	public static HashMap<String, String> getVariables(String input) {
		String tempStr = input.substring(2, input.length() - 2);
		String[] splitArr = tempStr.split(",");
		HashMap<String, String> variableMapping = new HashMap<String, String>();
		for (int i = 0; i < splitArr.length; i++) {
			String current = splitArr[i].trim();// Q( f(x) , z )
			String variables = current.substring(2, current.length() - 1);// f(x)
																			// ,
																			// z
																			// ;
			String[] variablesArr = variables.split(",");// [ f(x) , z ]

			System.out.println("current is " + current);
			for (int j = 0; j < variablesArr.length; j++) {
				String currentVar = variablesArr[j].trim();// f(x)
				System.out.println("current var is " + currentVar);
				if (currentVar.contains("(")) {
					String[] arr1 = currentVar.split("("); // [f,x)]
					String[] arr2 = arr1[1].split(")");// [x]
					String var = arr2[0];// x
					String temp = arr2[0];
					if (!variableMapping.containsKey(var)) {
						numVar++;
						var = temp + numVar;
						variableMapping.put(temp, var);
					}

				} else // z
				{
					System.out.println("here");
					if (!variableMapping.containsKey(currentVar)) {
						System.out.println("in here");
						numVar++;
						variableMapping.put(currentVar, currentVar + numVar);
					}
				}
			}

		}
		System.out.println("numKeys is " + variableMapping.size());
		return variableMapping;
	}
	
	
	

	public static void main(String[] args) {

		String input = "$ xyz [ p(x) & T(y) ] & $ x [ P(x) ]";

		// System.out.println(renameVariables(input));

		input = "% xz [ ( ! P(x) & ( Q(x) & $ yw [ Q(y) & R(x,w) ] ) ] ";
		// ~ ( ! P(x) | ! Q(y) )

		//input = "! ( P(x) & ( Q(y) & T(y) ) )";
		//input = "! ( ( P(x) &  Q(y) ) & T(y) )";

		// System.out.println(renameVariables(input));

	//	input = "% xz [ ( ! P(x) & ( Q(x) & $ yw [ Q(y) & R(x,w) ] ) ] ";

//		input = "% xz [ ( ! P(x) & ( Q(x) & $ yw [ Q(y) & R(x,w) ] ) ) ] ";

		input = "$ x [ P(x) & % x [ Q(x) > ! P(x) ] ]";
		input = "% x [ P(x) = ( Q(x) & $ y [ Q(y) & R(y,x) ] ) ]";
		System.out.println(input);
		System.out.println(getCNF(input));
		// // String input = " % xyz [ p(x) & T(y) ] & % x [ P(x) ]";
		// System.out.println(input);
		// String afterSkelomization = skelomize(input);
		// System.out.println(afterSkelomization);
		// String afterDiscardUQ = discardUQ(afterSkelomization);
		// System.out.println(afterDiscardUQ);
		// String flatten = flatten(afterDiscardUQ);

		// String input = " % xyz [ p(x) & T(y) ] & % x [ P(x) ]";

		input = "! ( P(x) & ( Q(y) & T(y) ) )";
		input = "! ( P(x) & Q(y) )";
		input = "! ( ( P(x) &  Q(y) ) & T(y) )";
		input = "! ( ( P(x) & Q(y) ) | R(z) )";
		input = "! $ xy [ p(x) & q(y) ]";
		input = "{ { P(x) , q(x) } , { l(x) , t(x) } }";
		//input = "{ { P( f(x) , z ) , q(x) } , { l(x) , t(x) } }";
	//	System.out.println(input);
	//	System.out.println(standardizeApart(input));
		// System.out.println(pushNotInwards(input));
		// System.out.println(applyDeMorganNot(input));
		// System.out.println(applyDeMorganNot(notQuantifierHandler(input)));
		// System.out.println(applyDeMorgan1(input));
		// // String input = " % xyz [ p(x) & T(y) ] & % x [ P(x) ]";
		// System.out.println(input);
		// String afterSkelomization = skelomize(input);
		// System.out.println(afterSkelomization);
		// String afterDiscardUQ = discardUQ(afterSkelomization);
		// System.out.println(afterDiscardUQ);

		// System.out.println(input);
		// String afterSkelomization = skelomize(input);
		// System.out.println(afterSkelomization);
		// String afterDiscardUQ = discardUQ(afterSkelomization);
		// System.out.println(afterDiscardUQ);

		// String input = "[ Q(Y) = R(Z) ] | [ P(X) = ( P(Y) & P(Z) ) ]";
		// String input = "$ xy [ P(x) ] | $ x [ T(x) ]";
		// String input = "! ! P(X)";
		// String input =
		// "[ ! ! Q(Y) = R(Z) ] | [ ! ! P(X) = ( P(Y) & P(Z) ) ]";
		// System.out.println(removeDoubleNot(input));
		// System.out.println(mySplitFunc(input));
		// System.out.println(getCNF(input));
		// System.out.println(renameVariables(input));
		// String input = "P(X) = ( P(Y) & P(Z) ) ";
		// String input = "[ P(X) > Q(X) ]";
		// int c = 'z';
		// String input2 = removeIfAndOnlyIf(input);
		// System.out.println(removeIfAndOnlyIf(input2));
		// try {
		// System.out.println(unify("P(x; g(x); g(f(a)))", "P(f(u); v; v)"));
		// } catch (Exception e) {
		// // TODO Auto-generated catch block
		// e.printStackTrace();
		// }
	}

}